/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.semantic;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.Assertion;
import alloy.ast.Decl;
import alloy.ast.Decls;
import alloy.ast.Fact;
import alloy.ast.Formula;
import alloy.ast.FormulaPara;
import alloy.ast.FormulaSeq;
import alloy.ast.Formulas;
import alloy.ast.Function;
import alloy.ast.Id;
import alloy.ast.InvocablePara;
import alloy.ast.Location;
import alloy.ast.Module;
import alloy.ast.ModuleInfo;
import alloy.ast.Multiplicity;
import alloy.ast.Node;
import alloy.ast.Predicate;
import alloy.ast.Qualifiers;
import alloy.ast.QuantifiedFormula;
import alloy.ast.Quantifier;
import alloy.ast.SetMultExpr;
import alloy.ast.SigExpr;
import alloy.ast.Signature;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.ast.Variables;
import alloy.semantic.ExprTypeCheckVisitor.TypeCheckException;

/**
 * <p>
 * Alloy Analyzer<br>
 * Copyright (c) 2001<br>
 * Massachusetts Institute of Technology<br>
 * <p>
 * Class: FormulaTypeCheckVisitor<br>
 * owner: msridhar<br>
 * Interface status: unstable<br>
 * Implementation status: unstable<br>
 * <p>
 * Type check all formulas in a specification.
 */

public class FormulaTypeCheckVisitor extends ASTDepthFirstVisitor {


    /** the current module scope */
    private ModuleInfo _moduleInfo;

    /**
     * Typecheck the formulas of a module.  Set the current module
     * scope, and then typecheck all the module's
     * signatures, facts, functions, and assertions.
     * @param module_ the module to typecheck
     */
    public void visit(Module module_) {
        // set the current module scope
        String moduleName = module_.getName().nodeString();
        _moduleInfo = module_.getModuleInfo();

        // just visit all the children
        visit((Node)module_);
    }

    /**
     * Typecheck the formulas of a signature.  Desugar the formulas
     * in the signature's fact, and then typecheck them.
     * @param signature_ the signature whose formulas are to be typechecked
     */
    public void visit(Signature signature_) {
    //System.out.println("Desugaring fact for " + signature_);
        // first, desugar the fact
        // formula sequence f goes to
        // all this: Sig | f
        // where Sig is the name of the signature and all field names get the
    // prefix "this." unless they are already prefixed with "@"
        Fact sigFact = signature_.getFact();
        if (!sigFact.getFormula().getFormulas().isLeaf()) {

            FormulaSeq formulas = sigFact.getFormula();

        //System.out.println("  Sig fact: " + formulas.nodeString());

        // create the declaration
            Variables variables = new Variables();
            variables.addVariable(new Variable(new Id(Location.UNKNOWN, "this")));
            SigExpr sigExpr = signature_.toSigExpr();
            Decl thisDecl = new Decl(Location.UNKNOWN, new Qualifiers(), variables,
				     new SetMultExpr(Location.UNKNOWN, Multiplicity.NONE, sigExpr));

        // transform the fact as described above by prefixing "this." to field references
        VariableExpr thisVar = new VariableExpr(new Variable(new Id(Location.UNKNOWN, "this")));
        thisVar.setType(signature_.getUnionType());
        Formula desugaredFact = (Formula) formulas.applyReturnVisitor(new FieldRefExpandingVisitor(thisVar,
                                                       _moduleInfo));

            // create the quantified formula
            Decls decls = new Decls();
            decls.addDecl(thisDecl);
            QuantifiedFormula quantFormula = new QuantifiedFormula(Location.UNKNOWN,
                                                                   Quantifier.ALL,
                                                                   decls, desugaredFact, false);

            // replace the original formulas with the desugared version
            Location loc = formulas.getLocation();
            quantFormula.setLocation(loc);
            Formulas newFormulas = new Formulas(loc);
            newFormulas.addFormula(quantFormula);
            FormulaSeq newSeq = new FormulaSeq(loc, newFormulas);
            newSeq.annotateTransform("desugaring of attached signature fact");
            sigFact.setFormula(newSeq);
            //System.out.println("  Sig fact desugared: " + newSeq.nodeString());
        }
        sigFact.applyVisitor(this);
    }

    /**
     * typecheck an function's formulas.
     * @param function_ the function to be typechecked
     * @see #visit(InvocablePara)
     */
    public void visit(Function function_) {
        visit((InvocablePara)function_);
    }

    /**
     * typecheck an predicate's formulas.
     * @param predicate_ the predicate to be typechecked
     * @see #visit(InvocablePara)
     */
    public void visit(Predicate predicate_) {
        visit((InvocablePara)predicate_);
    }

    /**
     * typecheck an invocable's formulas.  Just typecheck the
     * formulas with the localscope holding the arguments and
     * type parameters.
     * @param invocable_ the invocable to be typechecked
     */
    public void visit(InvocablePara invocable_) {
        // typecheck the formulas with the local scope
        try {
            //System.out.println("invocable " + invocable_.nodeString());
            invocable_.setFormula((FormulaSeq)ExprTypeCheckVisitor.typecheckNode(
                                        invocable_.getFormula(),
					_moduleInfo,
                                        invocable_.getLocalScope()));
        } catch (TypeCheckException e) {} // do nothing, the user will see the error message
    }


    /**
     * typecheck a formula paragraph that is not a function.
     * @param formulaPara_ the formula paragraph to be typechecked
     */
    public void visit(FormulaPara formulaPara_) {
        LocalScope localScope = new LocalScope();
    formulaPara_.setLocalScope(localScope);
        // now, typecheck formulas with new local scope
        try {
            formulaPara_.setFormula((FormulaSeq)ExprTypeCheckVisitor.typecheckNode(formulaPara_.getFormula(),
										   _moduleInfo, localScope));
        } catch (TypeCheckException e) {} // do nothing, the user will see the error message
    }

    /**
     * typecheck a fact.
     * @param fact_ the fact to be typechecked
     * @see #visit(FormulaPara)
     */
    public void visit(Fact fact_) {
        //System.out.println("FormulaTypeCheckVisitor visiting fact");
        visit((FormulaPara)fact_);
    }

    /**
     * typecheck an assertion.
     * @param assertion_ the assertion to be typechecked
     * @see #visit(FormulaPara)
     */
    public void visit(Assertion assertion_) {
        //System.out.println("FormulaTypeCheckVisitor visiting assertion");
        visit((FormulaPara)assertion_);
    }

}

